hasproperty(ctxm(dot,al,d_2,id_2,cd_2),ctxm(dot,al,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(kappa_,al,d_2,id_2,cd_2),ctxm(kappa_,al,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(pi_,u,d_2,id_2,cd_2),ctxm(pi_,u,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(zeta_,u,d_2,id_2,cd_2),ctxm(zeta_,u,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(xi_,u,d_2,id_2,cd_2),ctxm(xi_,u,d_4,id_4,cd_4),gt60).

knows(ttp,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(ttp,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(ttp,ctxm(dot,is,ip,ip_is,ip_is)).
knows(ttp,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(ttp,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(ttp,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(ttp,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(ttp,ctxm(dot,ttp,kM,kM_ttp,kM_ttp)).
knows(ii,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(ii,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(ii,ctxm(dot,is,ip,ip_is,ip_is)).
knows(ii,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(ii,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(ii,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(ii,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(ii,ctxm(dot,ii,kM,kM_ii,kM_ii)).
knows(ii,ctxm(kappa_,al,i_ii,i_al_ii,i_al_ii)).
knows(ii,ctxm(kappa_,al,d_1,id_1,cd_1)).
knows(ii,ctxm(kappa_,al,d_2,id_2,cd_2)).
knows(ii,ctxm(kappa_,al,d_3,id_3,cd_3)).
knows(ii,ctxm(pi_,u,i_ii,i_al_ii,i_al_ii)).
knows(ii,ctxm(pi_,dot,n_c1_4,in_pi_n4,cn_pi_n4)).
knows(ii,ctxm(pi_,dot,n_c1_5,in_pi_n5,cn_pi_n5)).
knows(ii,ctxm(pi_,dot,n_c1_6,in_pi_n6,cn_pi_n6)).
knows(is,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(is,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(is,ctxm(dot,is,ip,ip_is,ip_is)).
knows(is,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(is,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(is,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(is,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(is,ctxm(dot,is,kM,kM_is,kM_is)).
knows(is,ctxm(mu_,al,i_is,i_al_is,i_al_is)).
knows(is,ctxm(mu_,al,d_5,id_5,cd_5)).
knows(is,ctxm(mu_,al,d_6,id_6,cd_6)).
knows(is,ctxm(eta_,u,i_is,i_al_is,i_al_is)).
knows(is,ctxm(eta_,dot,n_c2_4,in_eta_n4,cn_eta_n4)).
knows(is,ctxm(eta_,dot,n_c2_5,in_eta_n5,cn_eta_n5)).
knows(is,ctxm(eta_,dot,n_c2_6,in_eta_n6,cn_eta_n6)).
knows(bs,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(bs,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(bs,ctxm(dot,is,ip,ip_is,ip_is)).
knows(bs,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(bs,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(bs,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(bs,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(bs,ctxm(dot,bs,kM,kM_bs,kM_bs)).
knows(bs,ctxm(zeta_,u,d_7,id_71,cd_71)).
knows(bs,ctxm(xi_,u,d_7,id_72,cd_72)).
knows(bs,ctxm(zeta_,dot,n_1_b,in_zeta_n1b,cn_zeta_n1b)).
knows(bs,ctxm(zeta_,dot,n_2_b,in_zeta_n2b,cn_zeta_n2b)).
knows(bs,ctxm(xi_,dot,n_1_b,in_xi_n1b,cn_xi_n1b)).
knows(bs,ctxm(xi_,dot,n_2_b,in_xi_n2b,cn_xi_n2b)).
knows(al,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(al,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(al,ctxm(dot,is,ip,ip_is,ip_is)).
knows(al,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(al,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(al,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(al,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(al,ctxm(dot,al,i,i_al,i_al)).
knows(al,ctxm(dot,al,i_ii,i_al_ii,i_al_ii)).
knows(al,ctxm(dot,al,i_is,i_al_is,i_al_is)).
knows(al,ctxm(dot,al,d_1,id_1,cd_1)).
knows(al,ctxm(dot,al,d_2,id_2,cd_2)).
knows(al,ctxm(dot,al,d_3,id_3,cd_3)).
knows(al,ctxm(dot,al,d_5,id_5,cd_5)).
knows(al,ctxm(dot,al,d_6,id_6,cd_6)).
knows(al,ctxm(pi_,u,i_ii,i_al_ii,i_al_ii)).
knows(al,ctxm(eta_,u,i_is,i_al_is,i_al_is)).
knows(al,ctxm(zeta_,u,i,i_al,i_al)).
knows(al,ctxm(xi_,u,i,i_al,i_al)).
knows(al,ctxm(pi_,u,ip,ip_al_1,ip_al_1)).
knows(al,ctxm(eta_,u,ip,ip_al_2,ip_al_2)).
knows(al,ctxm(zeta_,u,ip,ip_al_3,ip_al_3)).
knows(al,ctxm(xi_,u,ip,ip_al_4,ip_al_4)).
knows(al,ctxm(pi_,dot,n_c1_1,in_pi_n1,cn_pi_n1)).
knows(al,ctxm(pi_,dot,n_c1_2,in_pi_n2,cn_pi_n2)).
knows(al,ctxm(pi_,dot,n_c1_3,in_pi_n3,cn_pi_n3)).
knows(al,ctxm(pi_,dot,n_c1_7,in_pi_n7,cn_pi_n7)).
knows(al,ctxm(eta_,dot,n_c2_1,in_eta_n1,cn_eta_n1)).
knows(al,ctxm(eta_,dot,n_c2_2,in_eta_n2,cn_eta_n2)).
knows(al,ctxm(eta_,dot,n_c2_3,in_eta_n3,cn_eta_n3)).
knows(al,ctxm(eta_,dot,n_c2_7,in_eta_n7,cn_eta_n7)).
knows(al,ctxm(zeta_,dot,n_v,in_z_v,cn_z_v)).
knows(al,ctxm(zeta_,dot,cnd,i_cnd,d_cnd)).
knows(al,ctxm(zeta_,dot,n,in_zeta_n,cn_zeta_n)).
knows(al,ctxm(zeta_,dot,n_1_1,in_zeta_n11,cn_zeta_n11)).
knows(al,ctxm(zeta_,dot,n_1_2,in_zeta_n12,cn_zeta_n12)).
knows(al,ctxm(zeta_,dot,n_1_3,in_zeta_n13,cn_zeta_n13)).
knows(al,ctxm(zeta_,dot,n_1_a,in_zeta_n1a,cn_zeta_n1a)).
knows(al,ctxm(zeta_,dot,n_2_1,in_zeta_n21,cn_zeta_n21)).
knows(al,ctxm(zeta_,dot,n_2_a,in_zeta_n2a,cn_zeta_n2a)).
knows(al,ctxm(xi_,dot,n_v,in_x_v,cn_x_v)).
knows(al,ctxm(xi_,dot,cnd,i_cnd,d_cnd)).
knows(al,ctxm(xi_,dot,n,in_xi_n,cn_xi_n)).
knows(al,ctxm(xi_,dot,n_1_1,in_xi_n11,cn_xi_n11)).
knows(al,ctxm(xi_,dot,n_1_2,in_xi_n12,cn_xi_n12)).
knows(al,ctxm(xi_,dot,n_1_3,in_xi_n13,cn_xi_n13)).
knows(al,ctxm(xi_,dot,n_1_a,in_xi_n1a,cn_xi_n1a)).
knows(al,ctxm(xi_,dot,n_2_1,in_xi_n21,cn_xi_n21)).
knows(al,ctxm(xi_,dot,n_2_a,in_xi_n2a,cn_xi_n2a)).

